Definitions | x:A. B(x), P Q, P & Q, A & B, isrcv(e), t T, Prop, Top, S T, P Q, P Q, t ...$L, T, True, P Q, x. t(x), SQType(T), {T}, b, islocal(k), isl(x), act(k), b, outr(x), true, false, if b t else f fi, x:A. B(x), Msg, emsg(e), Msg(M), msg(l;t;v), valtype(e), False, SqStable(P), x(s), Dec(P), Knd, e sends a, e receives a, Unit, , A, locl(a), lnk(e), tag(e), rcvtype(e), |
Lemmas | not wf, assert wf, es-first wf, inheres wf, es-state wf, es-loc wf, es-state-when wf, atom-free-es-state, es-send-atom wf, es-E wf, es-state-after wf, es-kind wf, es-valtype-kindtype, es-val wf, islocal wf, isl wf, es-kindtype wf, locl wf, actof wf, unit wf, es-valtype wf, outl wf, isrcv wf, l member wf, es-Msg wf, es-sender wf, Id wf, Knd wf, event system wf, es-pred wf, state-after-pred, squash wf, true wf, es-loc-pred, inherence-ap-elim, atom-free-es-valtype, atom-free-Knd, atom-free-es-kindtype, inherence-trivial, sq stable atom-free, atom-free-es-Msg, atom-free-function, atom-free-settype, Knd sq, atom-free wf, atom-free-dep-function, atom-free-Id, decidable assert, es-isrcv wf, islocal-not-isrcv, assert of bnot, outl-inherence, false wf, atom-free-union, Id sq, subtype rel self, sq stable subtype rel, list-inherence, es-msg wf, atom-free-list, lnk wf, tagof wf, bool wf, eqtt to assert, es-rcvtype wf, iff transitivity, bnot wf, eqff to assert, es-M wf |